
Load RCC axioms and inverses

Show lemma1
=============================
Step 1

? (all x (all y (all z (((dc x y) & (tpp y z)) => (((dc x z) v (ec x z)) v ((po x z) v (pp x z)))))))


> revsk
=============================
Step 2

? (((~ (dc c155511 c155510)) v (~ (tpp c155510 c155509))) v (((dc c155511 c155509) v (ec c155511 c155509)) v ((po c155511 c155509) v (pp c155511 c155509))))


> hypdisj
=============================
Step 3

? (pp c155511 c155509)

1. (~ (po c155511 c155509))
2. (~ (ec c155511 c155509))
3. (~ (dc c155511 c155509))
4. (tpp c155510 c155509)
5. (dc c155511 c155510)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c155511 c155509)
|
|1. (~ (pp c155511 c155509))
|2. (~ (po c155511 c155509))
|3. (~ (ec c155511 c155509))
|4. (~ (dc c155511 c155509))
|5. (tpp c155510 c155509)
|6. (dc c155511 c155510)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c155509 c155511)
||
||1. (~ (p c155511 c155509))
||2. (~ (pp c155511 c155509))
||3. (~ (po c155511 c155509))
||4. (~ (ec c155511 c155509))
||5. (~ (dc c155511 c155509))
||6. (tpp c155510 c155509)
||7. (dc c155511 c155510)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c155511 c155509)
||||
||||1. (~ (p c155509 c155511))
||||2. (~ (p c155511 c155509))
||||3. (~ (pp c155511 c155509))
||||4. (~ (po c155511 c155509))
||||5. (~ (ec c155511 c155509))
||||6. (~ (dc c155511 c155509))
||||7. (tpp c155510 c155509)
||||8. (dc c155511 c155510)
||||
||||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||||=============================
|||||Step 7
|||||
|||||? (c c155511 c155509)
|||||
|||||1. (~ (o c155511 c155509))
|||||2. (~ (p c155509 c155511))
|||||3. (~ (p c155511 c155509))
|||||4. (~ (pp c155511 c155509))
|||||5. (~ (po c155511 c155509))
|||||6. (~ (ec c155511 c155509))
|||||7. (~ (dc c155511 c155509))
|||||8. (tpp c155510 c155509)
|||||9. (dc c155511 c155510)
|||||
|||||> ((c X Y) <-- (~ (dc X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (~ (dc c155511 c155509))
|||||
|||||1. (~ (c c155511 c155509))
|||||2. (~ (o c155511 c155509))
|||||3. (~ (p c155509 c155511))
|||||4. (~ (p c155511 c155509))
|||||5. (~ (pp c155511 c155509))
|||||6. (~ (po c155511 c155509))
|||||7. (~ (ec c155511 c155509))
|||||8. (~ (dc c155511 c155509))
|||||9. (tpp c155510 c155509)
|||||10. (dc c155511 c155510)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (ec c155511 c155509))
||||
||||1. (~ (o c155511 c155509))
||||2. (~ (p c155509 c155511))
||||3. (~ (p c155511 c155509))
||||4. (~ (pp c155511 c155509))
||||5. (~ (po c155511 c155509))
||||6. (~ (ec c155511 c155509))
||||7. (~ (dc c155511 c155509))
||||8. (tpp c155510 c155509)
||||9. (dc c155511 c155510)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (p c155511 c155509))
|||
|||1. (~ (p c155509 c155511))
|||2. (~ (p c155511 c155509))
|||3. (~ (pp c155511 c155509))
|||4. (~ (po c155511 c155509))
|||5. (~ (ec c155511 c155509))
|||6. (~ (dc c155511 c155509))
|||7. (tpp c155510 c155509)
|||8. (dc c155511 c155510)
|||
|||> hyp
||=============================
||Step 11
||
||? (~ (po c155511 c155509))
||
||1. (~ (p c155509 c155511))
||2. (~ (p c155511 c155509))
||3. (~ (pp c155511 c155509))
||4. (~ (po c155511 c155509))
||5. (~ (ec c155511 c155509))
||6. (~ (dc c155511 c155509))
||7. (tpp c155510 c155509)
||8. (dc c155511 c155510)
||
||> hyp
|=============================
|Step 12
|
|? (~ (pp c155509 c155511))
|
|1. (~ (p c155511 c155509))
|2. (~ (pp c155511 c155509))
|3. (~ (po c155511 c155509))
|4. (~ (ec c155511 c155509))
|5. (~ (dc c155511 c155509))
|6. (tpp c155510 c155509)
|7. (dc c155511 c155510)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 13
|
|? (~ (p c155509 c155511))
|
|1. (pp c155509 c155511)
|2. (~ (p c155511 c155509))
|3. (~ (pp c155511 c155509))
|4. (~ (po c155511 c155509))
|5. (~ (ec c155511 c155509))
|6. (~ (dc c155511 c155509))
|7. (tpp c155510 c155509)
|8. (dc c155511 c155510)
|
|> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
||=============================
||Step 14
||
||? (c Var96 c155509)
||
||1. (p c155509 c155511)
||2. (pp c155509 c155511)
||3. (~ (p c155511 c155509))
||4. (~ (pp c155511 c155509))
||5. (~ (po c155511 c155509))
||6. (~ (ec c155511 c155509))
||7. (~ (dc c155511 c155509))
||8. (tpp c155510 c155509)
||9. (dc c155511 c155510)
||
||> ((c Y X) <-- (p Z X) (c Y Z))
|||=============================
|||Step 15
|||
|||? (p Var99 c155509)
|||
|||1. (~ (c Var96 c155509))
|||2. (p c155509 c155511)
|||3. (pp c155509 c155511)
|||4. (~ (p c155511 c155509))
|||5. (~ (pp c155511 c155509))
|||6. (~ (po c155511 c155509))
|||7. (~ (ec c155511 c155509))
|||8. (~ (dc c155511 c155509))
|||9. (tpp c155510 c155509)
|||10. (dc c155511 c155510)
|||
|||> ((p X Y) <-- (pp X Y))
|||=============================
|||Step 16
|||
|||? (pp Var99 c155509)
|||
|||1. (~ (p Var99 c155509))
|||2. (~ (c Var96 c155509))
|||3. (p c155509 c155511)
|||4. (pp c155509 c155511)
|||5. (~ (p c155511 c155509))
|||6. (~ (pp c155511 c155509))
|||7. (~ (po c155511 c155509))
|||8. (~ (ec c155511 c155509))
|||9. (~ (dc c155511 c155509))
|||10. (tpp c155510 c155509)
|||11. (dc c155511 c155510)
|||
|||> ((pp X Y) <-- (tpp X Y))
|||=============================
|||Step 17
|||
|||? (tpp Var99 c155509)
|||
|||1. (~ (pp Var99 c155509))
|||2. (~ (p Var99 c155509))
|||3. (~ (c Var96 c155509))
|||4. (p c155509 c155511)
|||5. (pp c155509 c155511)
|||6. (~ (p c155511 c155509))
|||7. (~ (pp c155511 c155509))
|||8. (~ (po c155511 c155509))
|||9. (~ (ec c155511 c155509))
|||10. (~ (dc c155511 c155509))
|||11. (tpp c155510 c155509)
|||12. (dc c155511 c155510)
|||
|||> hyp
||=============================
||Step 18
||
||? (c c155510 c155510)
||
||1. (~ (c c155510 c155509))
||2. (p c155509 c155511)
||3. (pp c155509 c155511)
||4. (~ (p c155511 c155509))
||5. (~ (pp c155511 c155509))
||6. (~ (po c155511 c155509))
||7. (~ (ec c155511 c155509))
||8. (~ (dc c155511 c155509))
||9. (tpp c155510 c155509)
||10. (dc c155511 c155510)
||
||> ((c X X) <--)
|=============================
|Step 19
|
|? (~ (c c155510 c155511))
|
|1. (p c155509 c155511)
|2. (pp c155509 c155511)
|3. (~ (p c155511 c155509))
|4. (~ (pp c155511 c155509))
|5. (~ (po c155511 c155509))
|6. (~ (ec c155511 c155509))
|7. (~ (dc c155511 c155509))
|8. (tpp c155510 c155509)
|9. (dc c155511 c155510)
|
|> ((~ (c Y X)) <-- (~ (c X Y)))
|=============================
|Step 20
|
|? (~ (c c155511 c155510))
|
|1. (c c155510 c155511)
|2. (p c155509 c155511)
|3. (pp c155509 c155511)
|4. (~ (p c155511 c155509))
|5. (~ (pp c155511 c155509))
|6. (~ (po c155511 c155509))
|7. (~ (ec c155511 c155509))
|8. (~ (dc c155511 c155509))
|9. (tpp c155510 c155509)
|10. (dc c155511 c155510)
|
|> ((~ (c X Y)) <-- (dc X Y))
|=============================
|Step 21
|
|? (dc c155511 c155510)
|
|1. (c c155511 c155510)
|2. (c c155510 c155511)
|3. (p c155509 c155511)
|4. (pp c155509 c155511)
|5. (~ (p c155511 c155509))
|6. (~ (pp c155511 c155509))
|7. (~ (po c155511 c155509))
|8. (~ (ec c155511 c155509))
|9. (~ (dc c155511 c155509))
|10. (tpp c155510 c155509)
|11. (dc c155511 c155510)
|
|> hyp
=============================
Step 22

? (~ (p c155509 c155511))

1. (~ (pp c155511 c155509))
2. (~ (po c155511 c155509))
3. (~ (ec c155511 c155509))
4. (~ (dc c155511 c155509))
5. (tpp c155510 c155509)
6. (dc c155511 c155510)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 23
|
|? (c Var114 c155509)
|
|1. (p c155509 c155511)
|2. (~ (pp c155511 c155509))
|3. (~ (po c155511 c155509))
|4. (~ (ec c155511 c155509))
|5. (~ (dc c155511 c155509))
|6. (tpp c155510 c155509)
|7. (dc c155511 c155510)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 24
||
||? (p Var117 c155509)
||
||1. (~ (c Var114 c155509))
||2. (p c155509 c155511)
||3. (~ (pp c155511 c155509))
||4. (~ (po c155511 c155509))
||5. (~ (ec c155511 c155509))
||6. (~ (dc c155511 c155509))
||7. (tpp c155510 c155509)
||8. (dc c155511 c155510)
||
||> ((p Z X) <-- (~ (c (f150458 Z X Y) Z)))
||=============================
||Step 25
||
||? (~ (c (f150458 Var117 c155509 Var120) Var117))
||
||1. (~ (p Var117 c155509))
||2. (~ (c Var114 c155509))
||3. (p c155509 c155511)
||4. (~ (pp c155511 c155509))
||5. (~ (po c155511 c155509))
||6. (~ (ec c155511 c155509))
||7. (~ (dc c155511 c155509))
||8. (tpp c155510 c155509)
||9. (dc c155511 c155510)
||
||> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|||=============================
|||Step 26
|||
|||? (p Var117 Var123)
|||
|||1. (c (f150458 Var117 c155509 Var120) Var117)
|||2. (~ (p Var117 c155509))
|||3. (~ (c Var114 c155509))
|||4. (p c155509 c155511)
|||5. (~ (pp c155511 c155509))
|||6. (~ (po c155511 c155509))
|||7. (~ (ec c155511 c155509))
|||8. (~ (dc c155511 c155509))
|||9. (tpp c155510 c155509)
|||10. (dc c155511 c155510)
|||
|||> ((p X Y) <-- (pp X Y))
|||=============================
|||Step 27
|||
|||? (pp Var117 Var123)
|||
|||1. (~ (p Var117 Var123))
|||2. (c (f150458 Var117 c155509 Var120) Var117)
|||3. (~ (p Var117 c155509))
|||4. (~ (c Var114 c155509))
|||5. (p c155509 c155511)
|||6. (~ (pp c155511 c155509))
|||7. (~ (po c155511 c155509))
|||8. (~ (ec c155511 c155509))
|||9. (~ (dc c155511 c155509))
|||10. (tpp c155510 c155509)
|||11. (dc c155511 c155510)
|||
|||> ((pp X Y) <-- (tpp X Y))
|||=============================
|||Step 28
|||
|||? (tpp Var117 Var123)
|||
|||1. (~ (pp Var117 Var123))
|||2. (~ (p Var117 Var123))
|||3. (c (f150458 Var117 c155509 Var120) Var117)
|||4. (~ (p Var117 c155509))
|||5. (~ (c Var114 c155509))
|||6. (p c155509 c155511)
|||7. (~ (pp c155511 c155509))
|||8. (~ (po c155511 c155509))
|||9. (~ (ec c155511 c155509))
|||10. (~ (dc c155511 c155509))
|||11. (tpp c155510 c155509)
|||12. (dc c155511 c155510)
|||
|||> hyp
||=============================
||Step 29
||
||? (~ (c (f150458 c155510 c155509 Var120) c155509))
||
||1. (c (f150458 c155510 c155509 Var120) c155510)
||2. (~ (p c155510 c155509))
||3. (~ (c Var114 c155509))
||4. (p c155509 c155511)
||5. (~ (pp c155511 c155509))
||6. (~ (po c155511 c155509))
||7. (~ (ec c155511 c155509))
||8. (~ (dc c155511 c155509))
||9. (tpp c155510 c155509)
||10. (dc c155511 c155510)
||
||> ((~ (c (f150458 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 30
||
||? (~ (p c155510 c155509))
||
||1. (c (f150458 c155510 c155509 Var120) c155509)
||2. (c (f150458 c155510 c155509 Var120) c155510)
||3. (~ (p c155510 c155509))
||4. (~ (c Var114 c155509))
||5. (p c155509 c155511)
||6. (~ (pp c155511 c155509))
||7. (~ (po c155511 c155509))
||8. (~ (ec c155511 c155509))
||9. (~ (dc c155511 c155509))
||10. (tpp c155510 c155509)
||11. (dc c155511 c155510)
||
||> hyp
|=============================
|Step 31
|
|? (c c155510 c155510)
|
|1. (~ (c c155510 c155509))
|2. (p c155509 c155511)
|3. (~ (pp c155511 c155509))
|4. (~ (po c155511 c155509))
|5. (~ (ec c155511 c155509))
|6. (~ (dc c155511 c155509))
|7. (tpp c155510 c155509)
|8. (dc c155511 c155510)
|
|> ((c X X) <--)
=============================
Step 32

? (~ (c c155510 c155511))

1. (p c155509 c155511)
2. (~ (pp c155511 c155509))
3. (~ (po c155511 c155509))
4. (~ (ec c155511 c155509))
5. (~ (dc c155511 c155509))
6. (tpp c155510 c155509)
7. (dc c155511 c155510)

> ((~ (c Y X)) <-- (~ (c X Y)))
=============================
Step 33

? (~ (c c155511 c155510))

1. (c c155510 c155511)
2. (p c155509 c155511)
3. (~ (pp c155511 c155509))
4. (~ (po c155511 c155509))
5. (~ (ec c155511 c155509))
6. (~ (dc c155511 c155509))
7. (tpp c155510 c155509)
8. (dc c155511 c155510)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 34

? (dc c155511 c155510)

1. (c c155511 c155510)
2. (c c155510 c155511)
3. (p c155509 c155511)
4. (~ (pp c155511 c155509))
5. (~ (po c155511 c155509))
6. (~ (ec c155511 c155509))
7. (~ (dc c155511 c155509))
8. (tpp c155510 c155509)
9. (dc c155511 c155510)

> hyp

Show lemma2
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c161196 c161195)) v ((tpp c161196 c161195) v (ntpp c161196 c161195)))


> hypdisj
=============================
Step 3

? (ntpp c161196 c161195)

1. (~ (tpp c161196 c161195))
2. (pp c161196 c161195)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f155588 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c161196 c161195)
|
|1. (~ (ntpp c161196 c161195))
|2. (~ (tpp c161196 c161195))
|3. (pp c161196 c161195)
|
|> hyp
=============================
Step 5

? (~ (ec (f155588 c161196 c161195 Var32) c161196))

1. (~ (ntpp c161196 c161195))
2. (~ (tpp c161196 c161195))
3. (pp c161196 c161195)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c161196 Var36)
||
||1. (ec (f155588 c161196 c161195 Var32) c161196)
||2. (~ (ntpp c161196 c161195))
||3. (~ (tpp c161196 c161195))
||4. (pp c161196 c161195)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f155588 c161196 c161195 Var32) c161195)
|
|1. (ec (f155588 c161196 c161195 Var32) c161196)
|2. (~ (ntpp c161196 c161195))
|3. (~ (tpp c161196 c161195))
|4. (pp c161196 c161195)
|
|> ((ec (f155588 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c161196 c161195))
||
||1. (~ (ec (f155588 c161196 c161195 Var32) c161195))
||2. (ec (f155588 c161196 c161195 Var32) c161196)
||3. (~ (ntpp c161196 c161195))
||4. (~ (tpp c161196 c161195))
||5. (pp c161196 c161195)
||
||> hyp
|=============================
|Step 9
|
|? (pp c161196 c161195)
|
|1. (~ (ec (f155588 c161196 c161195 Var32) c161195))
|2. (ec (f155588 c161196 c161195 Var32) c161196)
|3. (~ (ntpp c161196 c161195))
|4. (~ (tpp c161196 c161195))
|5. (pp c161196 c161195)
|
|> hyp
=============================
Step 10

? (~ (tpp c161196 c161195))

1. (ec (f155588 c161196 c161195 Var32) c161196)
2. (~ (ntpp c161196 c161195))
3. (~ (tpp c161196 c161195))
4. (pp c161196 c161195)

> hyp

Finally prove main theorem

=============================
Step 1

? (all x (all y (all z (((dc x y) & (tpp y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (dc c167034 c167033)) v (~ (tpp c167033 c167032))) v (((((dc c167034 c167032) v (ec c167034 c167032)) v (po c167034 c167032)) v (tpp c167034 c167032)) v (ntpp c167034 c167032)))


> hypdisj
=============================
Step 3

? (ntpp c167034 c167032)

1. (~ (tpp c167034 c167032))
2. (~ (po c167034 c167032))
3. (~ (ec c167034 c167032))
4. (~ (dc c167034 c167032))
5. (tpp c167033 c167032)
6. (dc c167034 c167033)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c167034 c167032)
|
|1. (~ (ntpp c167034 c167032))
|2. (~ (tpp c167034 c167032))
|3. (~ (po c167034 c167032))
|4. (~ (ec c167034 c167032))
|5. (~ (dc c167034 c167032))
|6. (tpp c167033 c167032)
|7. (dc c167034 c167033)
|
|> ((pp Y Z) <-- (dc Y X) (tpp X Z) (~ (dc Y Z)) (~ (ec Y Z)) (~ (po Y Z)))
|||||=============================
|||||Step 5
|||||
|||||? (dc c167034 Var32)
|||||
|||||1. (~ (pp c167034 c167032))
|||||2. (~ (ntpp c167034 c167032))
|||||3. (~ (tpp c167034 c167032))
|||||4. (~ (po c167034 c167032))
|||||5. (~ (ec c167034 c167032))
|||||6. (~ (dc c167034 c167032))
|||||7. (tpp c167033 c167032)
|||||8. (dc c167034 c167033)
|||||
|||||> hyp
||||=============================
||||Step 6
||||
||||? (tpp c167033 c167032)
||||
||||1. (~ (pp c167034 c167032))
||||2. (~ (ntpp c167034 c167032))
||||3. (~ (tpp c167034 c167032))
||||4. (~ (po c167034 c167032))
||||5. (~ (ec c167034 c167032))
||||6. (~ (dc c167034 c167032))
||||7. (tpp c167033 c167032)
||||8. (dc c167034 c167033)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (dc c167034 c167032))
|||
|||1. (~ (pp c167034 c167032))
|||2. (~ (ntpp c167034 c167032))
|||3. (~ (tpp c167034 c167032))
|||4. (~ (po c167034 c167032))
|||5. (~ (ec c167034 c167032))
|||6. (~ (dc c167034 c167032))
|||7. (tpp c167033 c167032)
|||8. (dc c167034 c167033)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (ec c167034 c167032))
||
||1. (~ (pp c167034 c167032))
||2. (~ (ntpp c167034 c167032))
||3. (~ (tpp c167034 c167032))
||4. (~ (po c167034 c167032))
||5. (~ (ec c167034 c167032))
||6. (~ (dc c167034 c167032))
||7. (tpp c167033 c167032)
||8. (dc c167034 c167033)
||
||> hyp
|=============================
|Step 9
|
|? (~ (po c167034 c167032))
|
|1. (~ (pp c167034 c167032))
|2. (~ (ntpp c167034 c167032))
|3. (~ (tpp c167034 c167032))
|4. (~ (po c167034 c167032))
|5. (~ (ec c167034 c167032))
|6. (~ (dc c167034 c167032))
|7. (tpp c167033 c167032)
|8. (dc c167034 c167033)
|
|> hyp
=============================
Step 10

? (~ (tpp c167034 c167032))

1. (~ (ntpp c167034 c167032))
2. (~ (tpp c167034 c167032))
3. (~ (po c167034 c167032))
4. (~ (ec c167034 c167032))
5. (~ (dc c167034 c167032))
6. (tpp c167033 c167032)
7. (dc c167034 c167033)

> hyp
